From 8a119afd68f41a644904de45357b9b4ce441d7ee Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 16 Jun 2009 21:57:36 +0000
Subject: [PATCH] avoid fixing non-recursive terms

---
 helm/software/components/grafite_engine/grafiteEngine.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 1a88b0be1..98bfef9d6 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -814,7 +814,12 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
                     | NReference.Decl as s -> s))
                 | t -> NCicUtils.map (fun _ () -> ()) () fix t
               in
-              let obj_kind = NCicUntrusted.map_obj_kind (fix ()) obj_kind in
+              let obj_kind = 
+                match obj_kind with
+                | NCic.Fixpoint _ -> 
+                    NCicUntrusted.map_obj_kind (fix ()) obj_kind 
+                | _ -> obj_kind
+              in
               let obj = uri,height,[],[],obj_kind in
                NCicTypeChecker.typecheck_obj obj;
                let timestamp = NCicLibrary.add_obj uri obj in
-- 
2.39.2